import sys
import pystp

vc = pystp.Stp()

# vc_setFlags('a');
# vc_setFlags('w');
# vc_setFlags('r');
vc.setFlags("vsn")

# vc_push(vc);
e12866 = vc.varExpr("at", vc.createType(pystp.TYPE_BITVECTOR, 5))
e12867 = e12866
e12868 = vc.bvConstExprFromStr("10000")
e12869 = vc.eqExpr(e12867, e12868)
e12870 = vc.varExpr("x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e12871 = e12870
e12872 = vc.bvConstExprFromStr("00000000")
e12873 = vc.sbvGtExpr(e12871, e12872)

e12874 = vc.andExpr([e12869, e12873])
e12875 = vc.varExpr("lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e12876 = e12875
e12877 = e12870
e12878 = vc.iteExpr(vc.bvBoolExtract(e12876, 0), vc.bvRightShiftExpr(1 << 0, e12877), e12877)
e12879 = vc.iteExpr(vc.bvBoolExtract(e12876, 1), vc.bvRightShiftExpr(1 << 1, e12878), e12878)
e12880 = vc.iteExpr(vc.bvBoolExtract(e12876, 2), vc.bvRightShiftExpr(1 << 2, e12879), e12879)
e12881 = vc.bvConstExprFromStr("00000001")
e12882 = vc.eqExpr(e12880, e12881)
e12883 = vc.impliesExpr(e12874, e12882)
e12884 = e12866
e12885 = vc.eqExpr(vc.bvExtract(e12884, 0, 0), vc.bvConstExprFromStr("1"))
e12886 = vc.varExpr("k", vc.createType(pystp.TYPE_BITVECTOR, 8))
e12887 = e12886
e12888 = vc.eqExpr(vc.bvExtract(e12887, 7, 7), vc.bvConstExprFromStr("1"))
e12889 = vc.notExpr(e12888)
e12890 = e12866
e12891 = vc.eqExpr(vc.bvExtract(e12890, 4, 4), vc.bvConstExprFromStr("1"))
e12892 = vc.orExpr([e12889, e12891])
e12893 = vc.orExpr([e12885, e12892])
e12894 = vc.trueExpr()
e12895 = vc.andExpr([e12893, e12894])
e12896 = vc.andExpr([e12883, e12895])
e12897 = e12866
e12898 = vc.bvConstExprFromStr("00001")
e12899 = vc.eqExpr(e12897, e12898)
e12900 = e12886
e12901 = vc.bvConstExprFromStr("00000000")
e12902 = vc.sbvGeExpr(e12900, e12901)
e12903 = vc.andExpr([e12899, e12902])
e12904 = vc.varExpr("_at", vc.createType(pystp.TYPE_BITVECTOR, 5))
e12905 = e12904
e12906 = vc.bvConstExprFromStr("00010")
e12907 = vc.eqExpr(e12905, e12906)
e12908 = vc.varExpr("_lambda", vc.createType(pystp.TYPE_BITVECTOR, 8))
e12909 = e12908
e12910 = e12875
e12911 = vc.eqExpr(e12909, e12910)
e12912 = vc.andExpr([e12907, e12911])
e12913 = vc.varExpr("_x", vc.createType(pystp.TYPE_BITVECTOR, 8))
e12914 = e12913
e12915 = e12870
e12916 = vc.eqExpr(e12914, e12915)
e12917 = vc.andExpr([e12912, e12916])
e12918 = vc.varExpr("_y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e12919 = e12918
e12920 = vc.varExpr("y", vc.createType(pystp.TYPE_BITVECTOR, 8))
e12921 = e12920
e12922 = vc.eqExpr(e12919, e12921)
e12923 = vc.andExpr([e12917, e12922])
e12924 = vc.varExpr("_k", vc.createType(pystp.TYPE_BITVECTOR, 8))
e12925 = e12924
e12926 = e12886
e12927 = vc.eqExpr(e12925, e12926)
e12928 = vc.andExpr([e12923, e12927])
e12929 = vc.andExpr([e12903, e12928])
e12930 = e12866
e12931 = vc.bvConstExprFromStr("00001")
e12932 = vc.eqExpr(e12930, e12931)
e12933 = e12886
e12934 = vc.bvConstExprFromStr("00000000")
e12935 = vc.sbvGeExpr(e12933, e12934)
e12936 = vc.notExpr(e12935)
e12937 = vc.andExpr([e12932, e12936])
e12938 = e12904
e12939 = vc.bvConstExprFromStr("10000")
e12940 = vc.eqExpr(e12938, e12939)
e12941 = e12908
e12942 = e12875
e12943 = vc.eqExpr(e12941, e12942)
e12944 = vc.andExpr([e12940, e12943])
e12945 = e12913
e12946 = e12870
e12947 = vc.eqExpr(e12945, e12946)
e12948 = vc.andExpr([e12944, e12947])
e12949 = e12918
e12950 = e12920
e12951 = vc.eqExpr(e12949, e12950)
e12952 = vc.andExpr([e12948, e12951])
e12953 = e12924
e12954 = e12886
e12955 = vc.eqExpr(e12953, e12954)
e12956 = vc.andExpr([e12952, e12955])
e12957 = vc.andExpr([e12937, e12956])
e12958 = vc.orExpr([e12929, e12957])
e12959 = e12866
e12960 = vc.bvConstExprFromStr("00010")
e12961 = vc.eqExpr(e12959, e12960)
e12962 = e12920
e12963 = e12886
e12964 = vc.bvLeftShiftExpr(3, e12963)
e12965 = vc.bvConstExprFromStr("111100001100110010101010")
e12966 = vc.iteExpr(vc.bvBoolExtract(e12964, 0), vc.bvRightShiftExpr(1 << 0, e12965), e12965)
e12967 = vc.iteExpr(vc.bvBoolExtract(e12964, 1), vc.bvRightShiftExpr(1 << 1, e12966), e12966)
e12968 = vc.iteExpr(vc.bvBoolExtract(e12964, 2), vc.bvRightShiftExpr(1 << 2, e12967), e12967)
e12969 = vc.iteExpr(vc.bvBoolExtract(e12964, 3), vc.bvRightShiftExpr(1 << 3, e12968), e12968)
e12970 = vc.bvExtract(e12969, 7, 0)
e12971 = vc.bvAndExpr(e12962, e12970)
e12972 = vc.bvConstExprFromStr("00000000")
e12973 = vc.eqExpr(e12971, e12972)
e12974 = vc.notExpr(e12973)
e12975 = vc.andExpr([e12961, e12974])
e12976 = e12904
e12977 = vc.bvConstExprFromStr("00100")
e12978 = vc.eqExpr(e12976, e12977)
e12979 = e12908
e12980 = e12875
e12981 = vc.eqExpr(e12979, e12980)
e12982 = vc.andExpr([e12978, e12981])
e12983 = e12913
e12984 = e12870
e12985 = vc.eqExpr(e12983, e12984)
e12986 = vc.andExpr([e12982, e12985])
e12987 = e12918
e12988 = e12920
e12989 = vc.eqExpr(e12987, e12988)
e12990 = vc.andExpr([e12986, e12989])
e12991 = e12924
e12992 = e12886
e12993 = vc.eqExpr(e12991, e12992)
e12994 = vc.andExpr([e12990, e12993])
e12995 = vc.andExpr([e12975, e12994])
e12996 = vc.orExpr([e12958, e12995])
e12997 = e12866
e12998 = vc.bvConstExprFromStr("00010")
e12999 = vc.eqExpr(e12997, e12998)
e13000 = e12920
e13001 = e12886
e13002 = vc.bvLeftShiftExpr(3, e13001)
e13003 = vc.bvConstExprFromStr("111100001100110010101010")
e13004 = vc.iteExpr(vc.bvBoolExtract(e13002, 0), vc.bvRightShiftExpr(1 << 0, e13003), e13003)
e13005 = vc.iteExpr(vc.bvBoolExtract(e13002, 1), vc.bvRightShiftExpr(1 << 1, e13004), e13004)
e13006 = vc.iteExpr(vc.bvBoolExtract(e13002, 2), vc.bvRightShiftExpr(1 << 2, e13005), e13005)
e13007 = vc.iteExpr(vc.bvBoolExtract(e13002, 3), vc.bvRightShiftExpr(1 << 3, e13006), e13006)
e13008 = vc.bvExtract(e13007, 7, 0)
e13009 = vc.bvAndExpr(e13000, e13008)
e13010 = vc.bvConstExprFromStr("00000000")
e13011 = vc.eqExpr(e13009, e13010)
e13012 = vc.andExpr([e12999, e13011])
e13013 = e12904
e13014 = vc.bvConstExprFromStr("01000")
e13015 = vc.eqExpr(e13013, e13014)
e13016 = e12908
e13017 = e12875
e13018 = vc.eqExpr(e13016, e13017)
e13019 = vc.andExpr([e13015, e13018])
e13020 = e12913
e13021 = e12870
e13022 = vc.eqExpr(e13020, e13021)
e13023 = vc.andExpr([e13019, e13022])
e13024 = e12918
e13025 = e12920
e13026 = vc.eqExpr(e13024, e13025)
e13027 = vc.andExpr([e13023, e13026])
e13028 = e12924
e13029 = e12886
e13030 = vc.eqExpr(e13028, e13029)
e13031 = vc.andExpr([e13027, e13030])
e13032 = vc.andExpr([e13012, e13031])
e13033 = vc.orExpr([e12996, e13032])
e13034 = e12866
e13035 = vc.bvConstExprFromStr("00100")
e13036 = vc.eqExpr(e13034, e13035)
e13037 = e12908
e13038 = e12875
e13039 = e12886
e13040 = vc.bvConstExprFromStr("00000001")
e13041 = vc.iteExpr(vc.bvBoolExtract(e13039, 0), vc.bvExtract(vc.bvLeftShiftExpr(1, e13040), 8, 1), e13040)
e13042 = vc.iteExpr(vc.bvBoolExtract(e13039, 1), vc.bvExtract(vc.bvLeftShiftExpr(2, e13041), 9, 2), e13041)
e13043 = vc.iteExpr(vc.bvBoolExtract(e13039, 2), vc.bvExtract(vc.bvLeftShiftExpr(4, e13042), 11, 4), e13042)
e13044 = vc.bvPlusExpr(8, e13038, e13043)
e13045 = vc.eqExpr(e13037, e13044)
e13046 = e12918
e13047 = e12886
e13048 = vc.bvConstExprFromStr("00000001")
e13049 = vc.iteExpr(vc.bvBoolExtract(e13047, 0), vc.bvExtract(vc.bvLeftShiftExpr(1, e13048), 8, 1), e13048)
e13050 = vc.iteExpr(vc.bvBoolExtract(e13047, 1), vc.bvExtract(vc.bvLeftShiftExpr(2, e13049), 9, 2), e13049)
e13051 = vc.iteExpr(vc.bvBoolExtract(e13047, 2), vc.bvExtract(vc.bvLeftShiftExpr(4, e13050), 11, 4), e13050)
e13052 = e12920
e13053 = vc.iteExpr(vc.bvBoolExtract(e13051, 0), vc.bvRightShiftExpr(1 << 0, e13052), e13052)
e13054 = vc.iteExpr(vc.bvBoolExtract(e13051, 1), vc.bvRightShiftExpr(1 << 1, e13053), e13053)
e13055 = vc.iteExpr(vc.bvBoolExtract(e13051, 2), vc.bvRightShiftExpr(1 << 2, e13054), e13054)
e13056 = vc.eqExpr(e13046, e13055)
e13057 = vc.andExpr([e13045, e13056])
e13058 = e12904
e13059 = vc.bvConstExprFromStr("01000")
e13060 = vc.eqExpr(e13058, e13059)
e13061 = vc.andExpr([e13057, e13060])
e13062 = e12913
e13063 = e12870
e13064 = vc.eqExpr(e13062, e13063)
e13065 = vc.andExpr([e13061, e13064])
e13066 = e12924
e13067 = e12886
e13068 = vc.eqExpr(e13066, e13067)
e13069 = vc.andExpr([e13065, e13068])
e13070 = vc.andExpr([e13036, e13069])
e13071 = vc.orExpr([e13033, e13070])
e13072 = e12866
e13073 = vc.bvConstExprFromStr("01000")
e13074 = vc.eqExpr(e13072, e13073)
e13075 = e12924
e13076 = e12886
e13077 = vc.bvConstExprFromStr("00000001")
e13078 = vc.bvMinusExpr(8, e13076, e13077)
e13079 = vc.eqExpr(e13075, e13078)
e13080 = e12904
e13081 = vc.bvConstExprFromStr("00001")
e13082 = vc.eqExpr(e13080, e13081)
e13083 = vc.andExpr([e13079, e13082])
e13084 = e12908
e13085 = e12875
e13086 = vc.eqExpr(e13084, e13085)
e13087 = vc.andExpr([e13083, e13086])
e13088 = e12913
e13089 = e12870
e13090 = vc.eqExpr(e13088, e13089)
e13091 = vc.andExpr([e13087, e13090])
e13092 = e12918
e13093 = e12920
e13094 = vc.eqExpr(e13092, e13093)
e13095 = vc.andExpr([e13091, e13094])
e13096 = vc.andExpr([e13074, e13095])
e13097 = vc.orExpr([e13071, e13096])
e13098 = e12866
e13099 = vc.bvConstExprFromStr("10000")
e13100 = vc.eqExpr(e13098, e13099)
e13101 = e12904
e13102 = e12866
e13103 = vc.eqExpr(e13101, e13102)
e13104 = e12908
e13105 = e12875
e13106 = vc.eqExpr(e13104, e13105)
e13107 = vc.andExpr([e13103, e13106])
e13108 = e12913
e13109 = e12870
e13110 = vc.eqExpr(e13108, e13109)
e13111 = vc.andExpr([e13107, e13110])
e13112 = e12918
e13113 = e12920
e13114 = vc.eqExpr(e13112, e13113)
e13115 = vc.andExpr([e13111, e13114])
e13116 = e12924
e13117 = e12886
e13118 = vc.eqExpr(e13116, e13117)
e13119 = vc.andExpr([e13115, e13118])
e13120 = vc.andExpr([e13100, e13119])
e13121 = vc.orExpr([e13097, e13120])
e13122 = vc.andExpr([e12896, e13121])
e13123 = e12886
e13124 = vc.eqExpr(vc.bvExtract(e13123, 7, 7), vc.bvConstExprFromStr("1"))
e13125 = vc.notExpr(e13124)
e13126 = e12924
e13127 = vc.eqExpr(vc.bvExtract(e13126, 7, 7), vc.bvConstExprFromStr("1"))
e13128 = vc.notExpr(e13127)
e13129 = vc.notExpr(e13128)
e13130 = vc.andExpr([e13125, e13129])
e13131 = vc.andExpr([e13122, e13130])
vc.assertFormula(e13131)
# vc.push(vc)
e13132 = vc.falseExpr()
vc.query(e13132)
# vc.pop(vc)
# vc.pop(vc)
